In virtually all recognised branches of engineering, implementations are based on verified designs; that is, the functional requirements of the end product are specified rigorously, mathematical models are constructed to represent these requirements and the proposed designs, and the design models are mathematically verified against the requirements models to ensure that they fulfil their intended function before implementation starts.
Software is not generally developed this way. The majority of software systems are specified by informal requirements specifications that are written in natural language in business and domain specific terms by domain experts who are generally not experts in software design and implementation. It is widely recognised that such specifications suffer from incompleteness, ambiguity and inconsistencies; in other words, a lack of rigour and precision.
Designs are made by experts in software design and implementation, but whose background domain knowledge is frequently shallow or incomplete. As a consequence, they will frequently not recognise the shortcomings of the specifications they are working from until well into the implementation of testing phase of a project, if at all.
The behaviour of event driven, embedded software is often extremely complex with much use being made of parallelism and the design must address many issues related to concurrency. Errors in such designs are common because it is extremely difficult to understand and reason about concurrent systems. If undetected, such design errors lead to implementation errors that are extremely difficult to detect and diagnose by testing because they tend to be intermittent in their effect and difficult to reproduce.
As a result, it is common for such software to be released with a large number of undiscovered defects and for these to remain undetected for months or even years.
It is helpful to define a number of terms that are used throughout this specification for describing the known prior art approaches and the embodiments of the present invention (also referred to as the ASD system) and these are set out below:
Industrial Software:
Computer software developed primarily for commercial reasons. Such software is developed on a commercial basis and/or constitutes a product intended for commercial exploitation or constitutes a part of some other product itself developed on a commercial basis and/or intended for commercial exploitation.
Industrial software must meet the quality standards normally required and expected of commercial products in its market place. Industrial software usually needs to have a sustainable life of many years and be modifiable and maintainable by many different (teams of) software development experts during its life.
This is in contrast to software developed by academic, research or other organisations or individuals for non-commercial reasons such as advancing knowledge or for other reasons for which the primary motivation is not commercial.
Industrial Software Development:
Any activity to develop Industrial Software. Industrial software development is carried out in a business context and subject to cost and time-to-market constraints. It frequently takes many man-years of effort to develop and comprises of thousands to millions of lines of source program code and the specifications and designs embody extensive product and domain specific knowledge. The scale and complexity of industrial software development puts it beyond the capabilities of single individuals and requires teams of software development experts working together with product and domain specialists.
Industrial Software Design:
Design activities undertaken during industrial software development.
Black Box Specification:
The specification of the externally visible behaviour of software component in terms of a total mathematical function that maps every possible sequence of input stimuli to the appropriate response. The exact form of this function and its specification is given in [PP03]. In the ASD System, two varieties of Black Box Function Specifications are used:                1. An under-specified Black Box Function is used to specify component interfaces in a manner that captures the nondeterministic behaviour usually present on interface specifications because they are specified at a level of abstraction at which implementation details are hidden. In the ASD System, such specifications are also called Formal Interface Specifications.        2. A fully specified Black Box is used to specify the design of a component. It is always intended that component designs are deterministic at the level of abstraction at which the designed behaviour is specified. In the ASD System, such specifications are also called Formal Component Design Specifications.        
A Black Box Specification specifies behaviour in terms of sequences of input stimuli and responses. There is no state or control flow information included.
State Box Specification:
A State Box Specification is a recasting of a Black Box Specification in the form of a total mathematical function that maps a pair (state, stimuli) to a pair (new state, response). The sequences of input stimuli are replaced by state data capturing the same information. In the ASD System, State Box Specifications, also called Implementation Specifications, are required only for those parts of the software for which the program source code cannot be generated automatically by the Code Generator and must therefore be programmed by hand. A State Box must specify exactly the same behaviour as the Black Box from which it is derived.
Functional Requirements:
A set of statements specifying the required behaviour of a software component or system. Functional requirements are concerned only with behaviour; other required properties of the system or component are called non-functional requirements.
Functional Interface Specification:
An interface specification that describes the behaviour of a component in terms of its visible responses to sequences of input stimuli at one of its interfaces.
Requirements Specification:
A statement of requirements, functional and non-functional to be satisfied by the software system or component.
Architecture Specification:
A description of a software system that identifies its component parts, the interfaces between those components, the functions to be performed by each component and all other technical requirements and design rules with which all component designs and interface specifications must comply.
Component Specification and Design:
The detailed specification of a component, its organisation and structure and its detailed behaviour.
Component Test Cases:
Tests designed for testing specific individual components for correctness against the component specification and design. In the ASD System, these are typically generated automatically from the design by the Test Case Generator in the form of self executing test programs.
Source Program Code:
The implementation of the software in a programming language. This is not usually in a form that can be executed by a computer; it must first be translated to an executable form by special translators called compilers. A compiler is specific to the programming language being translated and the instruction set and architecture of the target computer processor.
Functional Design Specification:
A specification of a component design in terms of its behaviour.
Functional Correctness:
A design is said to be functionally correct if and only if the behaviour of the component complies with its Functional Requirements Specifications, the Functional Interface Specifications of the component interfaces it must implement and the component interfaces to other components that it uses.
It is also to be appreciated that the present specification references several academic papers and for the sake of convenience a fully referenced bibliography is provided at the end of the specific description.
Referring now to the block diagram of FIG. 1, there is shown a high-level summary of the essential phases of a conventional software development process 10 commonly used in industry. For the purposes of clarity, issues such as phases overlapping in practice and extending the description beyond the integration testing phase are ignored, as they are not relevant to the present invention. Additionally, all data/documents generated by any step are assumed to be carried through as input to all subsequent steps (for example, the informal requirements specification 14 is available to all five phases of the development process that follow the Requirements Analysis step 12). The steps taken for software development, as described in FIG. 1, are summarized as follows:                1. Requirements Analysis 12: Business analysts and domain experts develop Informal Requirements Specifications 14 describing, amongst other things, the required functional behaviour of the software system. This is written according to current practice and may use techniques such as UML diagrams, use cases, scenarios, sequence diagrams and flow charts together with natural language descriptions in an attempt to capture the essential behaviour as clearly as possible.        2. Specify and Design Architecture 16: Software design experts analyse the informal requirements 14 and partition the software system into components, identifying interfaces between them and allocating functional requirements to them. The result of this work is documented in an Informal Architecture Specification 18.        3. Specify and Design Components 20: For each component identified in the architecture 16, software design experts analyse the informal requirements and informal architecture specification and develop detailed specifications of the behaviour required of each component, their interfaces and a detailed design for implementing the required behaviour. The result of this work is a set of Informal Component Specifications and Designs documents 22.        4. Manually Implement Components 24: Software implementation experts write the Source Program Code 26 by hand, using all of the documents produced by the preceding steps. They also design and produce the detailed Component Test Cases 28 needed to test the programs, and detect and remove defects from them.        5. Component Testing 30: The source programs 26 implementing each component are tested individually and independently of each other using the component test cases 28 defined in the previous step. Depending on the nature of the components being implemented, the component testing 30 will be some mixture of automated test cases and manually executed test procedures. During this step, typically many errors are discovered in the program code. Some of these are implementation mistakes; others reflect errors made in earlier steps and are defects in the informal requirements, architecture and/or component designs and specifications. In FIG. 1, the consequences of this are depicted in the form of the Specification, Design and Implementation Defect Feedback Loops 32, 34. The resulting outputs of this step are Tested Components 36.        6. Integration Testing 38: In this step, the individually tested components 36 are integrated and tested to form the complete software system. During this step, a class of defects concerned with the interactions between the components are typically encountered for the first time. Due to issues such as concurrency, these are recognised as being among the most difficult to detect and solve. Some of these are implementation mistakes; others reflect errors made in earlier steps and are defects in the informal requirements, architecture and/or component designs and specifications. In FIG. 1, the consequences of this are depicted in the form of Specification, Design and Implementation Defect Feedback Loops 32, 34.        
As shown in FIG. 1, all specifications and designs are described as “informal”: they are not described in a rigorous notation based on mathematical principles. Consequently, (i) designs cannot be rigorously verified against their requirements specifications before implementation starts; and (ii) software developers rely on testing their implementation in order to detect errors in the original specifications and designs, as well as errors introduced during the implementation. FIG. 1 depicts this problem visually because the Specification and Design Defect Feedback Loops 32 connect all the phases of the software development process 10 together.
This way of carrying out conventional software design and its effects are illustrated graphically in FIGS. 2 and 3. FIG. 2 is a graph 50 showing how defects are commonly introduced throughout the software development process, but the majority of them are not detected and removed until testing starts late in the process. FIG. 3 is a graph 52, which depicts the consequences of the conventional approach on a typical project. As testing starts, defects are discovered and the amount of rework grows out of control.
As has been shown above there is a problem that errors in specifications and designs are not detected and removed before implementation and as a result, software testing must therefore detect and remove errors that originate in specification and designs, as well as errors of implementation. For software developed within industry, such a reliance on testing alone leads to unacceptable levels of defects remaining in the software. Some of the reasons for this, which have been appreciated by industry are summarized as follows:                1. Software testing can never be complete and cannot “prove” correctness; and        2. Industrial software is too complex to test exhaustively and therefore only a relatively small subset of total functionality can be tested.        
Broadly speaking, two major approaches have been taken to seek to address these problems:                Process-based approaches, where disciplined work flows are established and supported by appropriate management practices in an attempt to reduce the defects injected during specification and design phase. This is achieved by social techniques such as document reviews, design walk-throughs, code inspections and so on;        Formal method-based approaches, where mathematical techniques are used to specify requirements and designs and perform some mathematically based correctness verification before implementation.        
The informal, process-based approaches have generally come from the software development industry itself. Their major weakness is their steadfast refusal to recognise the need for mathematics for specifying and verifying software designs before implementation. These approaches, although valuable as form of disciplined engineering process, still rely on informal methods of specifying requirements and designs and provide no means for analysing the dynamic behaviour of the proposed designs before implementation. They also tend to lead to a concentration on the correctness of individual components rather than systems as a whole and do not address the most difficult design issues of concurrency in large systems.
The formal method-based approaches have largely been developed within academia and are mathematically based. Typically, required behaviour is specified using a rigorous mathematical notation and designs are evolved by a process called Stepwise Refinement in which designs and eventually implementations are produced in series of small, correctness preserving steps, rather similar in concept to the way mathematical proofs are presented.
In theory, the formal methods approach has held for a number of years now the promise of addressing the problems described in the previous section. There are numerous formal methods that have been developed over the last several decades, which have the necessary mathematical theory for modelling the designs of software systems and reasoning about their correctness. In practice, however, formal methods are hardly ever encountered in the industrial work place. Some of the reasons for this that have been appreciated by the present inventors are summarized as follows:
Lack of integration into software process: There is a communication gap between the formal methods experts on the one hand and the business analysts and domain experts on the other. There is little in the way of common shared knowledge between them. Business analysts and domain experts are not generally experts in any specific formal method and cannot participate in the process of developing formal specifications. The experts in formal methods generally are not experts in the domain of the system being specified and implemented and will not be familiar with the business case underlying the product; they must rely for on business analysts and domain experts for this knowledge. This communication gap raises the following question: if the business analysts and domain experts who have the product specific knowledge cannot understand the formal specifications and the formal methods experts who wrote and understand the formal specifications do not have a sufficiently deep understanding of the product domain to be sure that no mistakes have been made, how can the formal specifications be validated? Those who understand them don't know enough and those who know enough don't understand them. This gap must be overcome in order to integrate a formal approach into a software development process in industry. There must be feedback loops to and from every stage of the development process, including the clients and the domain experts.
Resistance within industry: Software developers and their management are not accustomed to applying mathematics to software development and many lack the necessary education and training to do so. There is strong resistance among software developers to a formal approach and the costs of doing so are perceived as prohibitive by management. Currently, industry is dedicated to an approach based on defect detection and removal and is attempting to address the current problems by becoming more efficient in testing. The use of formal methods requires an attitude shift away from this approach to one focused on defect prevention, a practice common in all other branches of engineering and this change is very difficult to achieve.
The immaturity of formal methods and tools: The formal methods techniques and tools are immature and are not able to cope with industrial scale software developments. These represent significant technical problems which have not been solved. They are also serious obstacles to progression because without tooling, all proof obligations must be carried out by hand. This is both error-prone and infeasible, given the scale of modern software systems being developed.